b:, P, Q:Top. if x:b then P else Q fi  ~ if b then P else Q fi  

latex

ProofTree

Definitions	, t  T, Top, x:A. B(x), left + right, P  Q, Dec(P), b, bool-decider(b), x:AB(x), P  Q, s = t, , if p:P then A(p) else B fi , False, A, b, x:A  B(x), P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, bool-decider wf, decidable wf, assert wf, top wf, bool wf